\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$:Id, $T$:Type, ${\it ks}$:Knd List,\+
\\[0ex]${\it tr}$:($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$) \}$\rightarrow$State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$$T$$\rightarrow$$T$).
\-\\[0ex]${\it ds}$ $\parallel$ $x$ : $T$
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ ($\forall$$k$:Knd. ($k$ $\in$ ${\it ks}$) $\Rightarrow$ isrcv($k$) $\Rightarrow$ $i$ $=$ destination(lnk($k$)))
\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ Normal(${\it da}$)
\\[0ex]$\Rightarrow$ \=R{-}state{-}var($i$;${\it ds}$;${\it da}$;$x$;$T$;${\it ks}$;${\it tr}$)\+
\\[0ex]$\Vdash$ ${\it es}$.\=es{-}decls(${\it es}$;$i$;${\it ds}$;${\it da}$)\+
\\[0ex]$\Rightarrow$ \=vartype($i$;$x$) $\subseteq\rho$ $T$\+
\\[0ex]\& \=$\forall$$e$@$i$.\+
\\[0ex]$\forall$${\it e'}$$\geq$$e$.($x$ after ${\it e'}$) $=$ es{-}trans{-}state{-}from\{i:l\}(${\it es}$;${\it ks}$;${\it tr}$;$x$ when $e$;$e$;${\it e'}$) $\in$ $T$
\-\-\-\-
\end{tabbing}